Boolean satisfiability (SAT) has many applications in the area of electronic design automation (EDA), artificial intelligence (AI), and operations research (OR). For example, SAT can be used to simulate the core of many problems in the field of computer-aided design (CAD) of integrated circuits, including logic synthesis, functional verification, equivalence checking, timing analysis, and automatic test pattern generation (ATPG).
SAT solvers are configured to solve a SAT problem posed as a boolean formula. Given a boolean formula F over a set of variables V, the task of a SAT solver is to find an assignment to all variables in V such that the value of F under this assignment is true, or prove that one does not exist. Most SAT solvers require that the boolean formula to be inputted in conjunctive normal form (CNF). CNF is a propositional boolean formula that includes a conjunction (i.e., logical AND) of one or more clauses, where each clause is a disjunction (i.e., logical OR) of one or more literals.
A literal is either a positive or a negative occurrence of a boolean variable (e.g., x, or its negation, −x). A literal may have one of three values: true, false, or undefined. A clause in which one literal is undefined and all the rest are false is called a unit clause. A unit clause forces an assignment of true to the undefined literal to satisfy the formula.
Modern SAT solvers usually maintain a CNF database. The database is modified constantly during the solving process according to mechanisms such as conflict clause learning, boolean constraint propagation and clause deletion. As provided in further detail below, conflict clause learning provides a method for generating a conflict clause which “learns” the root causes (assignments to variables) of a conflict in order to avoid reaching the same conflict again.
More specifically, a conflict clause describes a combination of assignments that should not be repeated due to conflicts in variable assignments. The conflict clause is added to the clause database to help prune the search space that remains to be traversed. A conflict clause is, typically, generated by a chain of resolution steps. The series of conflict clauses generated by a SAT solver can be illustrated by a resolution graph (See FIG. 1, for example).
A resolution graph is generated based on a final conflicting clause and all the clauses that imply a value to a variable without making any decisions until an empty clause is generated. A resolution graph is a proof for unsatisfiability of the CNF formula. The leaves in the graph represent the unsat core. During the solving process, the SAT solver keeps, for each generated conflict clause, an ordered list of resolve sources (i.e., clauses that took part in generating the conflict clause). The set of all resolve sources can be represented by a resolve trace (not shown in FIG. 1).
Generally, it is impossible to know which clauses will be included in the resolution graph before the solving process is over. Therefore, conventional SAT solvers are configured to include all resolve sources for each conflict clause in the resolve trace. A SAT solver may generate hundreds of thousands of conflict clauses during an average run. As a result, a large number of I/O operations may be performed to generate the respective resolve sources in the resolve trace file.
The process of generating a resolve trace degrades the performance of the SAT solver. Further, since in most cases the resolve trace is written to a file, several hundreds of mega bytes of disk space are consumed to store the resolve trace generated during the solving process.
Conventional methods are available that can reduce the size of a resolve trace after the SAT solver has completed execution. Unfortunately, this solution does not solve the above-mentioned problems associated with the large size of the generated resolve trace during the SAT solver run. Systems and methods are needed that can reduce the size of the resolve trace on the fly.